es:ES, e, a:E. (a <loc e)  (b:E. first(b) & a = pred(b) & b  e ) 

latex

Definitions	P  Q, P & Q, t  T, P  Q, x:A. B(x), P  Q, E, e  e' , pred(e), first(e), b, A, Prop, A & B, x:A. B(x), (e <loc e'), False, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, 1of(t), , Trans x,y:T. E(x;y)
Lemmas	es-le-trans, es-pred-le, es-pred-locl, es-le-self, event system wf, es-locl-wellfnd, es-locl wf, not wf, assert wf, es-first wf, es-pred wf, es-le wf, es-E wf, es-locl-iff